theory BehBase imports Main
begin

class linpreorder = preorder +    --"linear preorder"
  fixes par::"'a \<Rightarrow> 'a \<Rightarrow> bool"
assumes linear: "x \<le> y \<or> y \<le> x"
    and axpar [simp]: "par x y = (x \<le> y \<and> y \<le> x)"
begin

notation (xsymbols) less     (infixl "\<prec>" 65)
notation (xsymbols) less_eq  (infixl "\<preceq>" 65)
notation (xsymbols) par      (infixl "\<parallel>" 65)

lemma lem_parpres: "x1 \<prec> y1 \<and> y1 \<parallel> y2 \<Longrightarrow> x1 \<prec> y2"
  using axpar by (metis less_le_trans)

end

locale Events_base =  --"events algebra with program-independent axioms"
fixes trace :: "'prg \<Rightarrow> 'tr \<Rightarrow> bool"
  and ev    :: "'tr \<Rightarrow> 'a::linpreorder \<Rightarrow> bool"
  and proc  :: "'pn \<Rightarrow> 'a \<Rightarrow> bool"

  and read :: "'m \<Rightarrow> 'a \<Rightarrow> bool"
  and writeto :: "'m \<Rightarrow> 'a \<Rightarrow> bool"
  and val :: "'a ~=> 'Atemporal"

  assumes axcompl: "trace pg tr \<and> ev tr e \<Longrightarrow> \<exists> p . proc p e"
  assumes axlin:   "trace pg tr \<and> ev tr e1 \<and> ev tr e2 \<Longrightarrow> 
                       \<exists> p . proc p e1 \<and> proc p e2 \<Longrightarrow> e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1"
  assumes axshare: "trace pg tr \<and> ev tr e1 \<and> ev tr e2 \<Longrightarrow> 
                       (read x e1 \<or> writeto x e1) \<and> (read x e2 \<or> writeto x e2) \<Longrightarrow> 
                          e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1"
  assumes axrw:    "trace pg tr \<and> ev tr e \<Longrightarrow> 
                      read x e \<and> val e = Some w \<Longrightarrow> 
                        \<exists> e' . ev tr e' 
                          \<and>  e'\<prec>e \<and> (writeto x e') \<and> (val e' = Some w)
                          \<and> (\<forall> e''. ev tr e'' \<and> e''\<preceq>e \<and> writeto x e'' \<longrightarrow> e'' \<preceq> e')"
  assumes axexclio: "trace pg tr \<and> ev tr e \<Longrightarrow> read x e \<and> writeto y e \<Longrightarrow> False"
begin

lemma lem_wbefr:
  fixes x e1 e2 k1 k2
  assumes a0: "trace pg tr \<and> ev tr e1 \<and> ev tr e2"
  and a1:"read x e1 \<and> val e1 = Some k1 \<and> read x e2 \<and> val e2 = Some k2 \<and> e1 \<preceq> e2 \<and> k1 \<noteq> k2"
  shows "\<exists> e . ev tr e \<and> e1 \<prec> e \<and> e \<prec> e2 \<and> writeto x e \<and> val e = Some k2"
proof -
  from a1 obtain e2' where b1:"ev tr e2' \<and> e2'\<prec>e2 \<and> writeto x e2' \<and> val e2' = Some k2 \<and> (\<forall> e''. ev tr e'' \<and> e''\<preceq>e2 \<and> writeto x e'' \<longrightarrow> e'' \<preceq> e2')" using a0 axrw by metis
  moreover from this a1 have "e1 \<prec> e2' \<or> e2' \<prec> e1" using a0 axshare by (metis the.simps)
  moreover have "e2' \<preceq> e1 \<Longrightarrow> False"
  proof -
    assume d1:"e2' \<preceq> e1"
    from a1 obtain e1' where d2:"ev tr e1' \<and> e1'\<prec>e1 \<and> writeto x e1' \<and> val e1' = Some k1 \<and> (\<forall> e''. ev tr e'' \<and> e''\<preceq>e1 \<and> writeto x e'' \<longrightarrow> e'' \<preceq> e1')" using a0 axrw by blast
    from d1 d2 b1 have d3:"e2' \<preceq> e1'" by blast
    from a1 d2 have "e1' \<preceq> e2" by (metis less_le_not_le order_trans)
    from this d2 b1 have d4:"e1' \<preceq> e2'" by blast
    from b1 d2 have "e1' = e2' \<or> e1' \<prec> e2' \<or> e2' \<prec> e1'" using a0 axshare by blast
    from this d3 d4 have "e1' = e2'" by (metis less_le_not_le)
    from this b1 d2 a1 show "False" by simp
  qed
  ultimately show ?thesis by (metis less_le_not_le)
qed

end

end
